da:fpf(Knd; k.Type), l:IdLnk, tg:Id, T:top.
sqequal(fpf-cap(es-dt(l; da); id-deq; tg; T); fpf-cap(da; Kind-deq; rcv(l,tg); T)) 

latex

Definitions

Knd, t  T, x. t(x), x:A. B(x), fpf(A; a.B(a)), IdLnk, Id, top, fpf-cap(f; eq; x; z), fpf-dom(eq; x; f), , guard(T), P  Q, sq_type(T), fpf-domain(f), rcv(l,tg), (x  l), es-dt(l; da), P  Q, P  Q, P  Q, Kind-deq, id-deq, b, prop{i:l}, x:A. B(x), , Unit, tag(k), lnk(k), eq_lnk(a; b), if b then t else f fi , isrcv(k), ff, A, b, False, P  Q, True, T, A c B, outl(x), compose-fpf(a; b; f), fpf-ap(f; eq; x)

Lemmas

false wf, squash wf, true wf, bool cases, not functionality wrt iff, assert-eq-lnk, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, bfalse wf, compose-fpf-dom, isrcv wf, ifthenelse wf, eq lnk wf, lnk wf, tagof wf, unit wf, it wf, iff imp equal bool, iff functionality wrt iff, member-fpf-domain, assert wf, fpf-dom wf, id-deq wf, Kind-deq wf, es-dt wf, l member wf, rcv wf, fpf-domain wf, fpf-trivial-subtype-top, bool sq, top wf, Id wf, IdLnk wf, fpf wf, Knd wf